Example Proposition 7 in [ Lucas - IC'06]

Summary: ExProp7_Luc06

• TPDB format
• OBJ format
• Positive results:
  1. CSDP
  2. Ferreira and Ribeiro's transformation
  3. Giesl and Middeldorp's transformation
  4. Lucas' transformation
  5. Zantema's transformation

ExProp7_Luc06 in TPDB format ( ExProp7_Luc06.trs):

			
(VAR X)
(STRATEGY CONTEXTSENSITIVE 
  (f 1)
  (0)
  (cons 1)
  (s 1)
  (p 1)
)
(RULES 
f(0) -> cons(0,f(s(0)))
f(s(0)) -> f(p(s(0)))
p(s(X)) -> X
)

The CS-TRS in OBJ format (file ExProp7_Luc06.obj):

			
obj ExProp7_Luc06 is
  sort S .
  op f : S -> S .
  op 0 : -> S .
  op cons : S S -> S [strat (1 0)] .
  op s : S -> S .
  op p : S -> S .
  vars X : S .
  eq f(0) = cons(0,f(s(0))) .
  eq f(s(0)) = f(p(s(0))) .
  eq p(s(X)) = X .
endo

Positive results

1. The µ-termination of ExProp7_Luc06 can be proved by using CSDPs (computed by MuTerm).
   
2. The µ-termination of ExProp7_Luc06 can be proved by using Ferreira and Ribeiro's transformation. The TRS ExProp7_Luc06_FR:

   					
   	f(0) -> cons(0,n__f(n__s(n__0)))
   	f(s(0)) -> f(p(s(0)))
   	p(s(X)) -> X
   	f(X) -> n__f(X)
   	s(X) -> n__s(X)
   	0 -> n__0
   	activate(n__f(X)) -> f(activate(X))
   	activate(n__s(X)) -> s(activate(X))
   	activate(n__0) -> 0
   	activate(X) -> X	
   	

   can be proved terminating by AProVE
   
3. The µ-termination of ExProp7_Luc06 can be proved by using Giesl and Middeldorp's transformation. The TRS ExProp7_Luc06_GM:

   					 
   	a__f(0) -> cons(0,f(s(0)))
   	a__f(s(0)) -> a__f(a__p(s(0)))
   	a__p(s(X)) -> mark(X)
   	mark(f(X)) -> a__f(mark(X))
   	mark(p(X)) -> a__p(mark(X))
   	mark(0) -> 0
   	mark(cons(X1,X2)) -> cons(mark(X1),X2)
   	mark(s(X)) -> s(mark(X))
   	a__f(X) -> f(X)
   	a__p(X) -> p(X)	
   	

   can be proved terminating by AProVE .
   
4. The µ-termination of ExProp7_Luc06 can be proved by using Lucas' transformation. The TRS ExProp7_Luc06_L:

   					
   	f(0) -> cons(0)
   	f(s(0)) -> f(p(s(0)))
   	p(s(X)) -> X	
   	

   can be proved terminating by AProVE
   
5. The µ-termination of ExProp7_Luc06 can be proved by using Zantema's transformation. The TRS ExProp7_Luc06_Z:

   					
   	f(0) -> cons(0,n__f(s(0)))
   	f(s(0)) -> f(p(s(0)))
   	p(s(X)) -> X
   	f(X) -> n__f(X)
   	activate(n__f(X)) -> f(X)
   	activate(X) -> X
   
   	
   	

   can be proved terminating by AProVE .